6. 状态机

状态机（State Machine） 是对 逐步过程 的抽象。

状态机本质上是定义在单一集合上的 二元关系，集合中的元素被称作 状态，该关系被称作 转移关系，转移关系图又被称作 状态图，其中的箭头就代表一次 转移，记作 $q\to r$。此外状态机还有一个 初始状态。

我们定义状态机的 执行 是指状态机可能具有的状态序列（可能无限），其满足对任意在状态序列中连续的的状态，存在转移 $p\to r$。我们称所有可以在执行中出现的状态都是 可达的。如果对于状态机的转移关系是一个 函数（每个状态至多转移至一个可能的后继状态），称其为 确定性状态机；与之相反存在状态有多个后继状态的称为 非确定性状态机。

状态机有一个重要性质是 保持不变性（Preserved Invariant），其定义为：设 $P$ 为一个关于状态的谓词，如果对任意状态 $q$，$r$ 满足 $P(q)$ 为真且存在转移 $q\to r$，则 $P(r)$ 为真，称谓词 $P$ 具有 保持不变性。

由保持不变性的定义，我们很容易得出 Floyd 不变性原理：如果某具有保持不变性的谓词 $P$ 对起始状态 $s$ 有 $P(s)$ 为真，则对于任意可达状态 $q$，$P(q)$ 为真。

容易发现，不变性原理就是归纳法在状态机上的描述。基本步骤是证明初始状态时谓词为真；归纳步骤是证明该谓词具有保持不变性。

计算机中的许多算法都可以被建模为状态机。正确的算法或程序具有两个重要性质：

• 偏序正确性：如果一个过程会终止并得到一个最终结果，则该最终结果是符合系统要求的正确结果。
• 终止性：过程总会终止。

偏序正确性常常通过构建保持不变式通过不变性原理证明，而终止性一般使用良序原理证明。我们接下来介绍一下终止性的相关内容。

我们定义一个将状态机中的各个状态映射到某个值（不一定是非负整数集，也可以是实数或不是数字）的函数 $f$，这被称作 派生变量（Derived Variable）。其类似于物理中的 势函数，负责衡量状态的 “规模”。

我们称一个派生变量是 严格递减的，当且仅当

类似的，一个派生变量是 弱递减的，当且仅当

类似还可以定义 严格递增 和 弱递增 两个概念。

基于良序原理，如果某个状态机存在值域为良序集合的严格递减的派生变量，则该状态机的执行一定会终止。